Nuprl Lemma : R-da-Rlist
11,40
postcript
pdf
i
:top,
L
:(top List).
sqequal(R-da(Rlist(
L
);
i
); reduce((
u
,
da
. fpf-join(Kind-deq; R-da(
u
;
i
);
da
)); fpf-empty;
L
))
latex
Definitions
t
T
,
Y
,
reduce(
f
;
k
;
as
)
,
Rlist(
L
)
,
R-da(
R
;
i
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
i:top, L:(top List).
u,da. fpf-join(Kind-deq; R-da(u; i); da)); fpf-empty; L)) i:top, L:(top List).
u,da. fpf-join(Kind-deq; R-da(u; i); da)); fpf-empty; L)) 
Tx:A. B(x)